import os
import simsym
import symtypes
import errno
import model
import signal
import ptypes

IntArray = symtypes.tdict(ptypes.PREF, simsym.SInt)

class PROCPRIOQUEUE(simsym.tstruct(
		qprio = symtypes.tdict(ptypes.PREF, ptypes.PRIO),
		procs = symtypes.tdict(simsym.SInt, ptypes.PREF),
                size = simsym.SInt
                )):
	def _declare_assumptions(self, assume):
		super(PROCPRIOQUEUE, self)._declare_assumptions(assume)
		x = simsym.SInt.var("x")
		assume(simsym.forall(x, simsym.implies(
			self.procs.contains(x),
			self.qprio.contains(self.procs._map[x])
			)))
		a = ptypes.PREF.var("a")
		b = ptypes.PREF.var("b")
		i = simsym.SInt.var("i")
		j = simsym.SInt.var("j")
		assume(simsym.forall([a,b], simsym.implies(
			simsym.symand([self.qprio.contains(a), self.qprio.contains(b),
				self.qprio._map[a] <= self.qprio._map[b]]),
				simsym.exists([i,j], simsym.symand([i <= j,
				self.procs._map[i] == a, self.procs._map[j] == b]))
		)))
	
	@model.methodwrap()
	def INIT(self):
		self.size = 0
		simsym.assume(self.qprio.empty)
		simsym.assume(self.procs.empty)
	
	@model.methodwrap(pid = ptypes.PREF, pprio = ptypes.PRIO)
	def EnqueuePROCPRIOQUEUE(self, pid, pprio):
		self.qprio._map[pid] = pprio

	@model.methodwrap()
	def NextFromPROCPRIOQUEUE(self):
		ret = self.procs._map[0]
		self.RemovePrioQueueElem(ret)
		return ret

	@model.methodwrap(pid = ptypes.PREF)
	def IsInPROCPRIOQUEUE(self, pid):
		return self.procs.contains(pid)

	@model.methodwrap()
	def IsEmptyPROCPRIOQUEUE(self):
		return self.size == 0

	@model.methodwrap(pid = ptypes.PREF)
	def PrioOfProcInPROCPRIOQUEUE(self, pid):
		return self.qprio._map[self.procs._map[pid]]

	@model.methodwrap(pid = ptypes.PREF)
	def RemovePrioQueueElem(self, pid):
		x = simsym.SInt.var("x")
		simsym.assume(simsym.forall(x, simsym.implies(
			self.procs.contains(x),
			self.qprio.contains(self.procs._map[x])
			)))
		a = ptypes.PREF.var("a")
		b = ptypes.PREF.var("b")
		i = simsym.SInt.var("i")
		j = simsym.SInt.var("j")
		simsym.assume(simsym.forall([a,b], simsym.implies(
			simsym.symand([self.qprio.contains(a), self.qprio.contains(b),
				self.qprio._map[a] <= self.qprio._map[b]]),
				simsym.exists([i,j], simsym.symand([i <= j,
				self.procs._map[i] == a, self.procs._map[j] == b]))
		)))

	@model.methodwrap(pid = ptypes.PREF, newprio = ptypes.PRIO)
	def reorderProcPrioQueue(self, pid, newprio):
		x = simsym.SInt.var("x")
		simsym.assume(simsym.forall(x, simsym.implies(
			self.procs.contains(x),
			self.qprio.contains(self.procs._map[x])
			)))
		a = ptypes.PREF.var("a")
		b = ptypes.PREF.var("b")
		i = simsym.SInt.var("i")
		j = simsym.SInt.var("j")
		simsym.assume(simsym.forall([a,b], simsym.implies(
			simsym.symand([self.qprio.contains(a), self.qprio.contains(b),
				self.qprio._map[a] <= self.qprio._map[b]]),
				simsym.exists([i,j], simsym.symand([i <= j,
				self.procs._map[i] == a, self.procs._map[j] == b]))
		)))


model_class = PROCPRIOQUEUE

